es:ES, Sys:AbsInterface(Top), f:sys-antecedent(es;Sys). fifo-antecedent(es;Sys;f)   

latex

Up	abstract chain replication
Definitions of Statement	fifo-antecedent(es;Sys;f)
Definitions	t  T, sys-antecedent(es;Sys), AbsInterface(A), E(X), s = t, ES, x:AB(x), x:A. B(x), {x:A| B(x)} , P  Q, x:A  B(x), b, left + right, Top, loc(e), Id, , f(a), e c e', a:A fp B(a), strong-subtype(A;B), <a, b>, E, e  X, let x,y = A in B(x;y), t.1, EState(T), , Type, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), !Void(), x:A.B(x), S  T, suptype(S; T), first(e), A, pred(e), x.A(x), x. t(x), P & Q, e loc e' , P  Q, (e <loc e'), Atom$n, fifo-antecedent(es;Sys;f)
Lemmas	es-interface wf, es-is-interface wf, es-loc wf, es-locl wf, es-le wf, es-causle wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, Id wf, EState wf, event system wf, assert wf, es-E wf, member wf, es-E-interface wf, sys-antecedent wf, subtype rel wf, es-E-interface-subtype rel